COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00005 00003		nodes1[x,u] ←
C00006 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source;
.cb AN INDUCTION PRINCIPLE FOR CYCLIC LIST STRUCTURES


	Cyclic or re-entrant list structures are second class citizens
in most LISPs.  They can be created using ⊗rplaca and ⊗rplacd, but most
LISPs can't print them, and special programs have to be written
to compute with them.  The main characteristic of such programs
is that they must carry along a list of nodes already visited that
is compared with the current node in order to avoid infinite
recursions.

	A basic predicate may be defined as follows:

!!a1:	%2isstruct x ← isstruct1[x,qnil]%1,

	%2isstruct1[x,u] ← qat x ∨ x ε u ∨ isstruct1[qa x, x.u] ∧ isstruct1[qd x, x.u]%1.

It may be compared with the corresponding predicate for ordinary
S-expressions, namely

!!a2:	%2issexp x ← qat x ∨ issexp qa x ∧ issexp qd x%1

and that for natural numbers, namely

!!a3:	%2isnatnum n ← n=0 ∨ isnatnum n%5-%1.

To each such predicate corresponds an induction schema, namely

!!a4:	%2∀x u.(qat x ∨ x ε u ∨ qF(qa x, x.u) ∧ qF(qd x, x.u) ⊃ qF(x,u))

		⊃ ∀x u.qF(x,u)%1

corresponding to

!!a5:	%2∀x.(qat x ∨ qF(qa x) ∧ qF(qd x) ⊃ qF(x)) ⊃ ∀x.qF(x)%1

and

!!a6:	%2∀n.(n = 0 ∨ qF(n%5-%2) ⊃ qF(n)) ⊃ ∀n.qF(n)%1.

	Consider a program for determining the number of nodes in a
cyclic structure, namely

!!a7:	%2count x ← qa count1[x,qnil],

	count1[x,u] ← qif qat x qthen 1.u qelse qif x ε u qthen 0.u

		qelse α{count1[qa x, x.u]α}[λw. α{qa w, qd wα}[λm v.
			α{count1[qd x, v]α}[λu1.[m + qa u1] . qd u1]]]%1.

The statement that it is total is, in the formalism of (Cartwright
and McCarthy 1978),

!!a8:	%2∀x u.isnatnum count1[x,u]%1.
	nodes1[x,u] ←
		qif x ε u qthen u
		qelse qif qat x qthen x.u
		qelse nodes1[qd x, nodes1[qa x, u]]

cyclic.lsp[e80,jmc]